$\forall$${\it es}$:ES, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $e$:E.
\\[0ex]($\forall$$x$:Id. vartype(loc($e$);$x$) $\subseteq\rho$ ${\it ds}$($x$)?Top)
\\[0ex]$\Rightarrow$ $\neg$first($e$)
\\[0ex]$\Rightarrow$ state after pred($e$) $=$ (state when $e$) $\in$ State(${\it ds}$)